Search Results

Documents authored by Herbelin, Hugo

Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2014
LIPIcs, Volume 39, TYPES'14, Complete Volume

Authors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
LIPIcs, Volume 39, TYPES'14, Complete Volume
Cite as

20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{herbelin_et_al:LIPIcs.TYPES.2014,
  title =	{{LIPIcs, Volume 39, TYPES'14, Complete Volume}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014},
  URN =		{urn:nbn:de:0030-drops-55047},
  doi =		{10.4230/LIPIcs.TYPES.2014},
  annote =	{Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2014.i
Front Matter, Table of Contents, Preface, Authors Index

Authors: Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
Front Matter, Table of Contents, Preface, Authors Index
Cite as

20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{herbelin_et_al:LIPIcs.TYPES.2014.i,
  author =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  title =	{{Front Matter, Table of Contents, Preface, Authors Index}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{i--x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.i},
  URN =		{urn:nbn:de:0030-drops-54888},
  doi =		{10.4230/LIPIcs.TYPES.2014.i},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Authors Index}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.169
The Rooster and the Syntactic Bracket

Authors: Hugo Herbelin and Arnaud Spiwack

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions toward from smaller sorts to bigger sorts via explicit type construction, as well as impredicative sorts. Type families in impredicative sorts are constructed with a bracketing operation. The necessary restrictions of pattern-matching from impredicative sorts to types are confined to the bracketing construct. This type theory gives an alternative presentation to the calculus of inductive constructions on which the Coq proof assistant is an implementation.
Cite as

Hugo Herbelin and Arnaud Spiwack. The Rooster and the Syntactic Bracket. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 169-187, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{herbelin_et_al:LIPIcs.TYPES.2013.169,
  author =	{Herbelin, Hugo and Spiwack, Arnaud},
  title =	{{The Rooster and the Syntactic Bracket}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{169--187},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.169},
  URN =		{urn:nbn:de:0030-drops-46318},
  doi =		{10.4230/LIPIcs.TYPES.2013.169},
  annote =	{Keywords: Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact